T:Type, as:T List, R:(TTProp).
(x:T. R(x,x))  l-ordered(T;x,y.R(x,y);as)  no_repeats(T;as) 

latex

Definitions	t  T, f(a), x(s1,s2), x:A. B(x), P  Q, l-ordered(T;x,y.R(x;y);L), False, A, s = t, Prop, x:AB(x), Void, x before y  l, P  Q, P & Q, P  Q, Type, type List, x,y. t(x;y), no_repeats(T;l)
Lemmas	l-ordered wf, not wf, no repeats iff, l before wf